00100	
00200	
02000	(DEFPROP TRYIT 
02100	 (LAMBDA NIL
02200	  (PROG (C P P* N N* LEFT RE CAND END R CNT)
02250	(SETQ CNT(ADD1(LENGTH CLAUSES)))
02300		(SETQ C CLAUSES)
02400	   L1   (COND ((ALLPOS (CAR C)) (SETQ P (CONS (CAR C) P))) (T (SETQ N (CONS (CAR C) N))))
02500		(SETQ C (CDR C))
02600		(COND (C (GO L1)))
02700		(SETQ N* N)
02800		(SETQ P* P)
02900		(SETQ LEFT T)(SETQ RE (CAR N*))(SETQ CAND P)(SETQ END P*)
03000		(GO L3)
03100	   L2
03150	(COND((NULL(CDR P*))(COND((NULL(CDR N*))(ERR @NOPROOF))(T(GO L2A))))
03162		((NULL(CDR N*))(SETQ LEFT T)) )
03175	   (COND (LEFT (SETQ P* (CDR P*)) (SETQ RE (CAR P*)) (SETQ CAND N) (SETQ END N*) (SETQ LEFT NIL)(GO L3)))
03200	L2A (SETQ N* (CDR N*)) (SETQ CAND P) (SETQ END P*) (SETQ RE (CAR N*)) (SETQ LEFT T)
03300	   L3   (COND ((NOT (HERE RE)) (GO L2)) ((NOT (HERE (CAR CAND))) (GO L4)))
03400		(SETQ R (COND (LEFT (RESOLVE1 (CAR CAND) RE)) (T (RESOLVE1 RE (CAR CAND)))))
03500		(COND ((NULL R) (GO L4)) ((MEMQ NIL R) (PROOF RE (CAR CAND)) (RETURN (QUOTE QED))))
03600	(SETQ C(EDIT CLAUSES R))
03700		(COND ((NULL C) (GO L4)))
03710	(CLAUSES2 C)
03715	(SETQ CNT(PLUS CNT(LENGTH C)))
03717	(SETQ XX11 CLAUSES)(SETQ YY11 C)
03720	(BAKSUB CLAUSES C)
03730	(BOOKEEP EE1 C(CONS RE(CAR CAND)))
03800	   L5   (COND ((ALLPOS (CAR C)) (NCONC P (LIST(CAR C)))) (T (NCONC N (LIST(CAR C)))))
03900		(SETQ C (CDR C))
04000		(COND (C (GO L5)))
04100	   L4   (COND ((TTYIN) (UPDATE CLAUSES)))
04200		(COND ((EQ CAND END) (GO L2)))
04300		(SETQ CAND (CDR CAND))
04400		(GO L3))) 
04500	EXPR)